\begin{nusmvCommand}{check\_pslspec} {Performs PSL model checking}

\cmdLine{check\_pslspec [-h] [-m | -o output-file] [-n number | -p
    \linebreak "\pslexpr [IN context]"] [-b [-i] [-g] [-1] [-k\linebreak
    bmc\_lenght] [-l loopback]]}

Depending on the characteristics of the PSL property and on the
options, the commands applies CTL-based model checking, or LTL-based,
possibily bounded model checking.

A \pslexpr to be checked can be specified at command line using option
\commandopt{p}. Alternatively, option \commandopt{n} can be used for
checking a particular formula in the property database. If neither
\commandopt{n} nor \commandopt{p} are used, all the PSLSPEC formulas
in the database are checked. If option \commandopt{b} is used, LTL
bounded model checking is applied, otherwise bdd-based model checking
is applied. For LTL bounded model checking, options \commandopt{k} and
\commandopt{l} can be used to define the maximum problem bound, and
the value of the loopback for the single generated problems
respectively; their values can be stored in the environment variables
\envvar{\it bmc\_lenght} and \envvar{\it bmc\_loopback}. Single
problems can be generated by using option \commandopt{1}. By using
option \commandopt{i} the incremental version of bounded model
checking is activated. Bounded model checking problems can be
generated and dumped in a file by using option \commandopt{g}.

\begin{cmdOpt}
\opt{-m}{ Pipes the output generated by the command in processing
      \code{PSLSPEC}{s} to the program specified by the \envvar{PAGER}
      shell variable if defined, else through the \unix command
      \shellcommand{more}.}

\opt{-o \parameter{\filename{\it output-file}}}{Writes the output
      generated by the command in processing \code{PSLSPEC}s to the file
      \filename{\it output-file}}

\opt{-p \parameter{"\pslexpr [IN context]"}}{ A PSL formula to be
      checked.  \code{context} is the module instance name which the
      variables in \pslexpr must be evaluated in.}

\opt{-n \parameter{\natnum{number}}}{ Checks the PSL property with
      index \natnum{number} in the property database.}

\opt{-b}{Applies SAT-based bounded model checking. The SAT solver to be used will
      be chosen according to the current value of the system variable
      \envvar{sat\_solver}.}

\opt{-i}{Applies incremental SAT-bounded model checking if available,
      i.e. if an incremental SAT solver has been linked to
      NuSMV. This option can be used only in combination with the
      option \commandopt{b}.}

\opt{-g}{Dumps DIMACS version of bounded model checking problem into a
      file whose name depends on the system variable
      \envvar{bmc\_dimacs\_filename}. This feature is not allowed in
      combination of the option \commandopt{i}.}

\opt{-1}{Generates a single bounded model checking problem with fixed
      bound and loopback values, it does not iterate incrementing the
      value of the problem bound.}

\opt{-k \parameter{\natnum{\it bmc\_length}}}{\natnum{\it bmc\_length}
      is the maximum problem bound to be checked. Only natural numbers
      are valid values for this option. If no value is given the
      environment variable \envvar{\it bmc\_length} is considered
      instead.}

\opt{-l \parameter{\set{\it loopback}{\range{0}{max\_length-1},
      \range{-1}{bmc\_length}, X, *}}}{The {\it loopback} value may
      be: }

      \tabItem{a natural number in (0, {\it max\_length-1}). A
      positive sign (`+') can be also used as prefix of the
      number. Any invalid combination of length and loopback will be
      skipped during the generation/solving process.}

      \tabItem{a negative number in (-1, -{\it bmc\_length}). In this
      case {\it loopback} is considered a value relative to {\it
      max\_length}.  Any invalid combination of length and loopback
      will be skipped during the generation/solving process.}

      \tabItem{the symbol `\varvalue{X}', which means ``no loopback".}
      \tabItem{the symbol `\varvalue{*}', which means ``all possible
      loopbacks from zero to {\it length-1}" If no value is given the
      environment variable \envvar{\it bmc\_loopback} is considered
      instead..}

\end{cmdOpt}

\end{nusmvCommand}


  